sys-antecedent(es;Sys) == {f:E(Sys)E(Sys)| x:E(Sys). f(x) c x}  

latex

---

clarification:

sys-antecedent(es;Sys)
== {f:es-E-interface(es;Sys)es-E-interface(es;Sys)| 
== {x:es-E-interface(es;Sys). es-causle(es;f(x);x)}  

latex

Up	abstract chain replication
Wellformedness Lemmas	sys-antecedent wf
Definitions	{x:A| B(x)} , x:AB(x), x:A. B(x), E(X), e c e', f(a)
FDL editor aliases	sys-antecedent